The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

ordered(Cons(x', Cons(x, xs))) → ordered[Ite](<(x', x), Cons(x', Cons(x, xs)))
ordered(Cons(x, Nil)) → True
ordered(Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
goal(xs) → ordered(xs)

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
ordered[Ite](True, Cons(x', Cons(x, xs))) → ordered(xs)
ordered[Ite](False, xs) → False

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
ordered(Cons(0, Cons(S(y10_1), xs))) →⁺ ordered(xs)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(0, Cons(S(y10_1), xs))].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)